;(set-option :sat.xor.solver true)
(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(declare-fun e () (_ BitVec 8))
(declare-fun f () (_ BitVec 8))
(declare-fun j () (_ BitVec 8))
(declare-fun g () (_ BitVec 8))
(declare-fun h () (_ BitVec 8))
(assert (bvuge (bvlshr ((_ zero_extend 24) h) ((_ zero_extend 24) (_ bv2 8))) (_ bv8 32)))
(assert (distinct ((_ zero_extend 24) g) (_ bv0 32)))
(assert (let ((?d ((_ zero_extend 24) b))
       (?j ((_ zero_extend 24) c))
       (?i ((_ zero_extend 24) j))
       (?l ((_ zero_extend 24) g))
       (?aa ((_ zero_extend 24) h)))
     (bvult
     (bvadd (_ bv616 32) (bvmul (_ bv4294967295 32) (bvadd ?aa ?l ?i ?j ?d (_ bv9 32))))
     (_ bv256 32))))
(assert (let ((?am ((_ zero_extend 24) a))
       (?j ((_ zero_extend 24) c))
       (?an ((_ zero_extend 24) d))
       (?ao ((_ zero_extend 24) e))
       (?ap ((_ zero_extend 24) f)))
     (distinct (bvadd ?ap ?ao ?an ?j ?am) (_ bv0 32))))
(check-sat)